x:T. P(x) == Case xm({y:T| P(y) }) of inl(z)  z ; inr(w)  "???" 

latex

---

clarification:

choicef(xm; T; x.P(x)) == Case xm({y:T| P(y) }) of inl(z)  z ; inr(w)  "???" 

latex

FDL editor aliases

choicef